(declare-const r1 Real)
(declare-const r5 Real)
(declare-const r6 Real)
(assert (or (distinct (- 0.0334 r1 833.719653 r5 0.0334) r6 r6)))
(check-sat)
